| Definitions |  x:A. B(x), P   Q, t  T, when-after(e;info;pred?;init;Trans;val), Y, A B,  A, False, i j, Prop,  , 1of(t), 2of(t), let x,y,z = a in t(x;y;z), time(e), loc(e),  b, P & Q, vartype(i;x), islocal(k), A & B, isl(x), act(k), valtype(i;a), outl(x), Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),   x. t(x), x,y. t(x;y), S  T, S  T, outr(x), if b t else f fi, lnk(k), tag(k), b, true, false, val(e), act(e), let x = a in b(x), V(i;k), kind(e), SQType(T), {T}, FairFifo, w-machine-constraint(w), w-automaton(T;TA;M), E, Knd, x(s), x(s1,s2),  , Unit, P  Q, rcv(l,tg),  , w.TA, w.M, locl(a) |
| Lemmas | fair-fifo wf, world wf, nat wf, w-loc-lemma, w-loc wf, Id sq, le wf, w-time wf, w-E wf, nat properties, ge wf, w-machine wf, w-automaton wf, w-T wf, w-TA wf, w-M wf, assert wf, w-isnull wf, w-a wf, not wf, Id wf, w-vartype wf, w-s wf, w-kind wf, w-val wf, subtype rel self, kindcase wf, IdLnk wf, islocal wf, isl wf, actof wf, unit wf, w-valtype wf, outl wf, Knd wf, false wf, true wf, Msg wf, w-m wf, lsrc wf, mlnk wf, first wf, w-pred wf, bool wf, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, w-stutter, w-first-null, w-kind-lemma, kind wf, w-info wf, pred wf, w-pred-decreases, w-loc-pred, let wf, pi2 wf, w-pred-null, w-eval wf |
w.T(loc(e),x))
(x:Id